﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Microsoft.Pex.Framework;
using Microsoft.Pex.Framework.Goals;
using PexMe.Attribute;
using Microsoft.Pex.Framework.Validation;

namespace MicroBenchmarks.ExternalClass
{
    [PexClass]
    public partial class ExternalClassTest
    {
        /// <summary>
        /// A scenario where the not-covered branching condition appears from the external
        /// method, but the actual situation is from the inner one. How to deal with this situation?
        /// </summary>
        /// <param name="os"></param>
        [PexAssertReachEventually]
        [PexMethod]
        [PexMe.Attribute.FieldAccessObserver]
        [PexMe.Attribute.InsufficientObjectFactoryObserver]
        [PexAllowedException(typeof(NullReferenceException))]
        public void ExternalClassTestPUT([PexAssumeUnderTest]MainClass os)
        {
            if (os.Size() > 2)
                PexAssert.ReachEventually();
        }
    }
}
